00100	∀E KW S,P,W;
00200	∀E REFLEX S,W;
00300	∀E KNOW S,NOT(P),W;
00400	∀E NOT W,P;
00500	ASSUME T(K(S,NOT(P)),W);
00600	TAUT  ∀W1.(A(S,W,W1)⊃T(NOT(P),W1)) 3,5;
00700	∀E ↑ W;
00800	⊃E 2,↑;
00900	⊃I 5⊃↑;
01000	TAUT (T(P,W)∧T(KW(S,P),W))⊃T(K(S,P),W) 1,4,9;
01100	∀I ↑ S P W;
01200	∀E KNOW S,P,W;
01300	ASSUME T(K(S,P),W);
01400	TAUT ∀W1.(A(S,W,W1)⊃T(P,W1)) 12:13;
01500	∀E ↑ W;
01600	⊃E 2,↑;
01700	⊃I 13⊃↑;
01800	∀I ↑ S P W;
01900	∀E FOOL FOOL,P,W;
02300	∀E FOOL S,K(FOOL,P),W;
02700	∀E 18 FOOL,K(S,K(FOOL,P)),W;
03300	TAUT T(K(FOOL,P),W)⊃T(K(S,K(FOOL,P)),W) 42:44;
03600	∀I ↑ S W P;
04000	∀E KNOW S,K(FOOL,P),W;
04400	ASSUME T(K(FOOL,P),W);
05000	TAUT ∀W1.(A(S,W,W1)⊃T(K(FOOL,P),W1)) 22 24:25
05200	∀E ↑ W1;
05600	⊃I ↑↑↑⊃↑;
06200	TAUT (T(K(FOOL,P),W)∧A(S,W,W1))⊃T(K(FOOL,P),W1) 28;
06500	∀I ↑ S P W W1;